(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const _11-0 (_ BitVec 11))
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const v22 Bool)
(assert (or v8 v8 v8 v8))
(assert (or v8))
(assert (or (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6)))
(assert (or v8 v8 v8 v8 v8 (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6)))
(assert (or (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6)))
(assert (or v8 v8 (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) v8))
(assert (or (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6)))
(assert (or (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6)))
(assert (or (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6)))
(assert (or v8 (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) v8 v8 (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) v8 (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) v8 (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) v8 (= (bvuge (bvshl _11-0 _11-0) _11-0) v12 v6) v8))
(check-sat)
